/*
 * SYmbolic Model-Based test case generation toOL for Real-Time systems (SYMBOLRT)
 * (C) Copyright 2010-2012 Federal University of Campina Grande (UFCG)
 * 
 * This file is part of SYMBOLRT.
 *
 * SYMBOLRT is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * SYMBOLRT is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with SYMBOLRT.  If not, see <http://www.gnu.org/licenses/>.
 *
 *
 * REVISION HISTORY:
 * Author                           Date           Brief Description
 * -------------------------------- -------------- ------------------------------
 * Wilkerson de Lucena Andrade      16/06/2011     An old class named TIOSTSPreprocessing (Version 1.2) was divided into two classes. This class only contains the synchronous algorithm algorithm (Version 1.0).
 * 
 */

package br.edu.ufcg.symbolrt.algorithms;

import java.util.Collection;
import java.util.List;

import br.edu.ufcg.symbolrt.base.Action;
import br.edu.ufcg.symbolrt.base.ClockGuard;
import br.edu.ufcg.symbolrt.base.Location;
import br.edu.ufcg.symbolrt.base.SimpleClockGuard;
import br.edu.ufcg.symbolrt.base.TIOSTS;
import br.edu.ufcg.symbolrt.base.Transition;
import br.edu.ufcg.symbolrt.base.TypedData;
import br.edu.ufcg.symbolrt.exception.IncompatibleOperationException;
import br.edu.ufcg.symbolrt.util.Constants;


/**
 * <code>SynchronousProduct</code> Class. <br>
 * This class contains an algorithm needed to perform the sequential composition between two TIOSTSs.
 * 
 * @author Adriana Carla Damasceno  ( <a href="mailto:adriana@copin.ufcg.edu.br">adriana@copin.ufcg.edu.br</a> )
 * 
 * @version 1.0
 * <br>
 * SYmbolic Model-Based test case generation toOL for Real-Time systems (SYMBOLRT)
 * <br>
 * (C) Copyright 2010-2012 Federal University of Campina Grande (UFCG)
 * <br>
 * <a href="https://sites.google.com/a/computacao.ufcg.edu.br/symbolrt">https://sites.google.com/a/computacao.ufcg.edu.br/symbolrt</a>
 */
public class SequentialComposition {

	private static SequentialComposition instance = null;

	private SequentialComposition() {
	}

	/**
	 * Method used to obtain an instance of this class.
	 * @return An instance of {@link SequentialComposition}.
	 */
	public static SequentialComposition getInstance() {
		if (instance == null) {
			instance = new SequentialComposition();
		}
		return instance;
	}

	/**
	 * Returns the sequential composition between two TIOSTSs.
	 * @param t1 The first TIOSTS.
	 * @param t1 The second TIOSTS.
	 * @return The sequential composition between t1 and t2.
	 * @throws IncompatibleSequentialComposition If t1 do not fit conditions demanded to it.  
	 */
	public TIOSTS sequentialComposition(TIOSTS model1, TIOSTS model2) throws IncompatibleOperationException {

		TIOSTS result = null;
		
		TIOSTS tiosts1 = model1.clone();
		TIOSTS tiosts2 = model2.clone();

		Location lc = getCompositionLocation(tiosts1);
		//Despising the init location
		Location l02 = tiosts2.getInitialLocation().getOutTransitions().get(0).getTarget();

		if (isCompatible(tiosts1, tiosts2, lc)){

			result = initialize(tiosts1, tiosts2);
		
			//Building the new set of independent transitions and locations from both models

			for(Transition transition1:tiosts1.getTransitions()){
				if (!transition1.getTarget().equals(lc)){
					result.addTransition(transition1);
					result.addLocation(transition1.getSource());
				}				
			}

			for(Transition transition2:tiosts2.getTransitions()){
				//Despising the l02 location and init location
				if (!transition2.getSource().equals(l02)&&(!transition2.getSource().equals(tiosts2.getInitialLocation()))){
					result.addTransition(transition2);
					result.addLocation(transition2.getTarget());
				}				
			}
			
			
			//Synchronizing models transitions
			
			Transition t1 = lc.getInTransitions().get(0);
			Transition t2 = l02.getOutTransitions().get(0);
			
			Action actionlc = t1.getAction();
			Action actionl02 = t2.getAction();
			
			Location source = new Location(t1.getSource().getLabel()+ "," + t2.getSource().getLabel());
			Location target = new Location(t1.getTarget().getLabel()+ "," + t2.getTarget().getLabel());
			result.addLocation(source);
			result.addLocation(target);
			String dataAssignments = createAssignments(t1.getDataAssignments(), t2.getDataAssignments());
			String clockAssignments = createAssignments(t1.getClockAssignments(), t2.getClockAssignments());
			//Performing the conjunction among the initial condition of tiosts2 and data conditions of transitions t1 and t2
			String dataGuard = createDataGuard(t1.getDataGuard(), t2.getDataGuard());
			dataGuard = createDataGuard(dataGuard, tiosts2.getInitialCondition());
			ClockGuard clockGuard = createClockGuard(t1.getClockGuard(), t2.getClockGuard());
			List<String> parameters = actionl02.getParameters();
			Action action = result.recoverAction(actionlc); 
			action.setParameters(parameters);
			result.createTransition(source.getLabel(), dataGuard, clockGuard, action, dataAssignments, clockAssignments, Constants.DEADLINE_EAGER, target.getLabel());
			
			
			//Updating references for synchronization node in the resulting model
			
			for(Transition resultingTransition: result.getTransitions()){
				if (resultingTransition.getTarget().equals(t1.getSource())){
					resultingTransition.setTarget(source);					
				}
				
				if (resultingTransition.getSource().equals(t2.getTarget())){
					resultingTransition.setSource(target);					
				}				
			}


		}

		return result;
	}

	private TIOSTS initialize (TIOSTS tiosts1, TIOSTS tiosts2){
		TIOSTS result = new TIOSTS(tiosts1.getName() +";"+tiosts2.getName());


		List<Action> internalActions;
		List<Action> outputActions;
		List<Action> inputActions;
		List<TypedData> variables;
		List<TypedData> parameters;
		List<String> clocks;
		result.setInitialCondition(tiosts1.getInitialCondition());
		result.setInitialLocation(tiosts1.getInitialLocation());

		//Performing union between input and output actions
		internalActions = tiosts1.getInternalActions();
		internalActions.addAll(tiosts2.getInternalActions());
		result.setInternalActions(internalActions);

		outputActions = tiosts1.getOutputActions();
		outputActions.addAll(tiosts2.getOutputActions());
		result.setOutputActions(outputActions);

		inputActions = tiosts1.getInputActions();
		inputActions.addAll(tiosts2.getInputActions());			
		result.setInputActions(inputActions);

		//Performing union between variables, parameters and clocks of t1 and t2

		variables = tiosts1.getVariables();
		variables.addAll(tiosts2.getVariables());
		result.setVariables(variables);

		parameters = tiosts1.getActionParameters();
		parameters.addAll(tiosts2.getActionParameters());
		result.setActionParameters(parameters);	

		clocks = tiosts1.getClocks();
		clocks.addAll(tiosts2.getClocks());
		result.setClocks(clocks);

		return result;
	}

	private boolean isCompatible(TIOSTS tiosts1, TIOSTS tiosts2, Location lc) throws IncompatibleOperationException{
		boolean resp = true;		

		if (lc != null){
			List<Transition> outputTransitionslc =  lc.getOutTransitions();
			List<Transition> inputTransitionslc = lc.getInTransitions();
			
			//Verifying that the composition node has one input and no output transitions
			if (!(outputTransitionslc.isEmpty() && inputTransitionslc.size() == 1)){
				throw new IncompatibleOperationException("The final node must not contain output transitions or it has more than one input transition.");
			}
			
			//Verifying that assignment is empty
						
			Action actionlf1 = inputTransitionslc.get(0).getAction();
			String assignmentslc1 = inputTransitionslc.get(0).getDataAssignments(); 
			
			
			if (assignmentslc1 != null){
				throw new IncompatibleOperationException("Assignments of the composition node must be empty.");								
			}
			
			//Verifying that deadline is eager
			
			String deadlinelc1 = inputTransitionslc.get(0).getDeadline();
			
			if (deadlinelc1 != "eager"){
				throw new IncompatibleOperationException("Deadline of the composition node must be eager.");								
			}
			
			// Verifying that action is a single output action in tiosts1
			resp = resp && isSingleAction(tiosts1, actionlf1, Constants.ACTION_OUTPUT);
			
			//Despising the init location of the second TIOSTS
			List<Transition> outputTransitionsInit2 = tiosts2.getInitialLocation().getOutTransitions();
			
			//Verifying that the initial location of tiosts2 has only one outgoing transition 		
			
			List<Transition> outputTransitionslo2 = outputTransitionsInit2.get(0).getTarget().getOutTransitions();
			Action actionl02 = outputTransitionslo2.get(0).getAction();
						
			if (!(outputTransitionslo2.size() == 1 && (actionl02.getType() == Constants.ACTION_INPUT))){
				throw new IncompatibleOperationException("There is more than one output transition after the initial location of the second TIOSTS or the transition has no input action.");
			}	
			
			// Verifying that actionl02 is a single input action in tiosts2
			resp = resp && isSingleAction(tiosts2, actionl02, Constants.ACTION_INPUT);
			
			//Verifying that actionl02 and actionlf1 have the same label
			if(actionlf1.getName() != actionl02.getName()){
				throw new IncompatibleOperationException("Actions of the first and second TIOSTS do not synchronize.");
			}
			
			//parameter matching between synchronizing actions of tiosts1 and tiosts2
			
			List<String> parameterslf1 = actionlf1.getParameters();
			List<String> parametersl02 = actionl02.getParameters();
			
			if (parameterslf1.size() != parametersl02.size()){
				throw new IncompatibleOperationException("The number of parameters between synchronizing actions of both TIOSTS must be equal.");
			}
			
		}else{
			throw new IncompatibleOperationException("There is no composition location.");
		}
			
		//Verifying that there is no intersection between locations of T1 and T2
		if (intersection(tiosts1.getLocationNames(), tiosts2.getLocationNames()) == true){			
			throw new IncompatibleOperationException("The set of locations from both TIOSTSs must be disjoint.");
		}
		
		//Verifying that there is no intersection between variables of T1 and T2
		if (intersection(tiosts1.getvariableNames(), tiosts2.getvariableNames()) == true){
			throw new IncompatibleOperationException("The set of variables from both TIOSTSs must be disjoint.");
		}	
		
		return resp;
	}


	private Location getCompositionLocation(TIOSTS tiosts) throws IncompatibleOperationException{
		Collection<Transition> transitions = tiosts.getTransitions();
		Collection<Location> locations = tiosts.getLocations();

		Location compositeLocation = null;
		for(Location l: locations){					

			//Verify if the current location l is source of a transition
			boolean foundOutgoingTransition = false;				
			for(Transition t:transitions){
				if (t.getSource() == l){
					foundOutgoingTransition = true;
				}
			}

			//If there is no location without outgoing transitions found, l is the one
			if (compositeLocation == null && foundOutgoingTransition == false){
				compositeLocation = l;
			}else{
				// If a location without outgoing transitions was found, the TIOSTS has more than one composite location, being out of our restrictions 
				if (compositeLocation != null && foundOutgoingTransition == false){
					throw new IncompatibleOperationException("Only one location without outgoing transitions is allowed");
				}
			}				
		}

		return compositeLocation;

	}
	
	private boolean isSingleAction(TIOSTS tiosts, Action action, int type) throws IncompatibleOperationException{
		boolean resp = true;
		
		if(action.getType() == type){
			boolean foundAction = false;
			for(Transition t:tiosts.getTransitions()){
				if (action.getName().equals(t.getAction().getName())){
					if (foundAction == false){
						foundAction = true;								
					}else{
						throw new IncompatibleOperationException("More than one action " + action.getName() + " was found in the TIOSTS.");
					}

				}

			}	

		}else{
			throw new IncompatibleOperationException("Some action type of a TIOSTS is wrong.");
		}		
		return resp;		
	}

	private boolean intersection(List<String> colecao1, List<String> colecao2){
		boolean isIntersection = false;

		for (String c:colecao1){
			if (colecao2.contains(c)){
				isIntersection = true;
			}
		}		

		return isIntersection;
	}
	
	/**
	 * Creates the assignments of a transition considering the assignments of specification and test purpose.
	 * @param specAssignments The assignments of a transition of specification.
	 * @param tpAssignments The assignments of a transition of test purpose.
	 * @return The assignment resulting from merging assignments of specification and test purpose. 
	 */
	private String createAssignments(String specAssignments, String tpAssignments){
		if (tpAssignments == null) {
			return specAssignments;
		} else if (specAssignments == null) {
			return tpAssignments;
		} else {
			return specAssignments + Constants.ASSIGNMENT_SEPARATOR + tpAssignments;
		}
	}

	/**
	 * Creates the data guard of a transition considering the guard of specification and test purpose.
	 * @param specGuard The guard of a transition of specification.
	 * @param tpGuard The guard of a transition of test purpose.
	 * @return The data guard resulting from conjunction of guards of specification and test purpose. 
	 */
	private String createDataGuard(String specGuard, String tpGuard){
		if (tpGuard == Constants.GUARD_TRUE) {
			return specGuard;
		} else if (specGuard == Constants.GUARD_TRUE){
			return tpGuard;
		} else {
			return specGuard + " " + Constants.GUARD_CONJUNCTION + " " + tpGuard;
		}
	}
	
	/**
	 * Creates the clock guard of a transition considering the guard of specification and test purpose.
	 * @param specGuard The guard of a transition of specification.
	 * @param tpGuard The guard of a transition of test purpose.
	 * @return The clock guard resulting from conjunction of guards of specification and test purpose. 
	 */
	// TODO Refatorar depois. Deve ir para a classe ClockGuard
	private ClockGuard createClockGuard(ClockGuard specGuard, ClockGuard tpGuard){
		ClockGuard newClockGuard = new ClockGuard();
		
		for (SimpleClockGuard simpleClockGuard : specGuard.getClockGuard()) {
			newClockGuard.addSimpleClockGuard(simpleClockGuard.clone());
		}
		
		for (SimpleClockGuard simpleClockGuard : tpGuard.getClockGuard()) {
			newClockGuard.addSimpleClockGuard(simpleClockGuard.clone());
		}
		return newClockGuard;
	}

}